Left Termination of the query pattern log2_in_2(a, g) w.r.t. the given Prolog program could not be shown:



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof

Clauses:

log2(X, Y) :- log2(X, 0, s(0), Y).
log2(s(s(X)), Half, Acc, Y) :- log2(X, s(Half), Acc, Y).
log2(X, s(s(Half)), Acc, Y) :- ','(small(X), log2(Half, s(0), s(Acc), Y)).
log2(X, Half, Y, Y) :- ','(small(X), small(Half)).
small(0).
small(s(0)).

Queries:

log2(a,g).

We use the technique of [30].Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

log2_in(X, Y) → U1(X, Y, log2_in(X, 0, s(0), Y))
log2_in(X, Half, Y, Y) → U5(X, Half, Y, small_in(X))
small_in(s(0)) → small_out(s(0))
small_in(0) → small_out(0)
U5(X, Half, Y, small_out(X)) → U6(X, Half, Y, small_in(Half))
U6(X, Half, Y, small_out(Half)) → log2_out(X, Half, Y, Y)
log2_in(X, s(s(Half)), Acc, Y) → U3(X, Half, Acc, Y, small_in(X))
U3(X, Half, Acc, Y, small_out(X)) → U4(X, Half, Acc, Y, log2_in(Half, s(0), s(Acc), Y))
log2_in(s(s(X)), Half, Acc, Y) → U2(X, Half, Acc, Y, log2_in(X, s(Half), Acc, Y))
U2(X, Half, Acc, Y, log2_out(X, s(Half), Acc, Y)) → log2_out(s(s(X)), Half, Acc, Y)
U4(X, Half, Acc, Y, log2_out(Half, s(0), s(Acc), Y)) → log2_out(X, s(s(Half)), Acc, Y)
U1(X, Y, log2_out(X, 0, s(0), Y)) → log2_out(X, Y)

The argument filtering Pi contains the following mapping:
log2_in(x1, x2)  =  log2_in(x2)
U1(x1, x2, x3)  =  U1(x3)
log2_in(x1, x2, x3, x4)  =  log2_in(x2, x3, x4)
0  =  0
s(x1)  =  s(x1)
U5(x1, x2, x3, x4)  =  U5(x4)
small_in(x1)  =  small_in
small_out(x1)  =  small_out(x1)
U6(x1, x2, x3, x4)  =  U6(x1, x4)
log2_out(x1, x2, x3, x4)  =  log2_out(x1)
U3(x1, x2, x3, x4, x5)  =  U3(x3, x4, x5)
U4(x1, x2, x3, x4, x5)  =  U4(x1, x5)
U2(x1, x2, x3, x4, x5)  =  U2(x5)
log2_out(x1, x2)  =  log2_out(x1)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
  ↳ PrologToPiTRSProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

log2_in(X, Y) → U1(X, Y, log2_in(X, 0, s(0), Y))
log2_in(X, Half, Y, Y) → U5(X, Half, Y, small_in(X))
small_in(s(0)) → small_out(s(0))
small_in(0) → small_out(0)
U5(X, Half, Y, small_out(X)) → U6(X, Half, Y, small_in(Half))
U6(X, Half, Y, small_out(Half)) → log2_out(X, Half, Y, Y)
log2_in(X, s(s(Half)), Acc, Y) → U3(X, Half, Acc, Y, small_in(X))
U3(X, Half, Acc, Y, small_out(X)) → U4(X, Half, Acc, Y, log2_in(Half, s(0), s(Acc), Y))
log2_in(s(s(X)), Half, Acc, Y) → U2(X, Half, Acc, Y, log2_in(X, s(Half), Acc, Y))
U2(X, Half, Acc, Y, log2_out(X, s(Half), Acc, Y)) → log2_out(s(s(X)), Half, Acc, Y)
U4(X, Half, Acc, Y, log2_out(Half, s(0), s(Acc), Y)) → log2_out(X, s(s(Half)), Acc, Y)
U1(X, Y, log2_out(X, 0, s(0), Y)) → log2_out(X, Y)

The argument filtering Pi contains the following mapping:
log2_in(x1, x2)  =  log2_in(x2)
U1(x1, x2, x3)  =  U1(x3)
log2_in(x1, x2, x3, x4)  =  log2_in(x2, x3, x4)
0  =  0
s(x1)  =  s(x1)
U5(x1, x2, x3, x4)  =  U5(x4)
small_in(x1)  =  small_in
small_out(x1)  =  small_out(x1)
U6(x1, x2, x3, x4)  =  U6(x1, x4)
log2_out(x1, x2, x3, x4)  =  log2_out(x1)
U3(x1, x2, x3, x4, x5)  =  U3(x3, x4, x5)
U4(x1, x2, x3, x4, x5)  =  U4(x1, x5)
U2(x1, x2, x3, x4, x5)  =  U2(x5)
log2_out(x1, x2)  =  log2_out(x1)


Using Dependency Pairs [1,30] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

LOG2_IN(X, Y) → U11(X, Y, log2_in(X, 0, s(0), Y))
LOG2_IN(X, Y) → LOG2_IN(X, 0, s(0), Y)
LOG2_IN(X, Half, Y, Y) → U51(X, Half, Y, small_in(X))
LOG2_IN(X, Half, Y, Y) → SMALL_IN(X)
U51(X, Half, Y, small_out(X)) → U61(X, Half, Y, small_in(Half))
U51(X, Half, Y, small_out(X)) → SMALL_IN(Half)
LOG2_IN(X, s(s(Half)), Acc, Y) → U31(X, Half, Acc, Y, small_in(X))
LOG2_IN(X, s(s(Half)), Acc, Y) → SMALL_IN(X)
U31(X, Half, Acc, Y, small_out(X)) → U41(X, Half, Acc, Y, log2_in(Half, s(0), s(Acc), Y))
U31(X, Half, Acc, Y, small_out(X)) → LOG2_IN(Half, s(0), s(Acc), Y)
LOG2_IN(s(s(X)), Half, Acc, Y) → U21(X, Half, Acc, Y, log2_in(X, s(Half), Acc, Y))
LOG2_IN(s(s(X)), Half, Acc, Y) → LOG2_IN(X, s(Half), Acc, Y)

The TRS R consists of the following rules:

log2_in(X, Y) → U1(X, Y, log2_in(X, 0, s(0), Y))
log2_in(X, Half, Y, Y) → U5(X, Half, Y, small_in(X))
small_in(s(0)) → small_out(s(0))
small_in(0) → small_out(0)
U5(X, Half, Y, small_out(X)) → U6(X, Half, Y, small_in(Half))
U6(X, Half, Y, small_out(Half)) → log2_out(X, Half, Y, Y)
log2_in(X, s(s(Half)), Acc, Y) → U3(X, Half, Acc, Y, small_in(X))
U3(X, Half, Acc, Y, small_out(X)) → U4(X, Half, Acc, Y, log2_in(Half, s(0), s(Acc), Y))
log2_in(s(s(X)), Half, Acc, Y) → U2(X, Half, Acc, Y, log2_in(X, s(Half), Acc, Y))
U2(X, Half, Acc, Y, log2_out(X, s(Half), Acc, Y)) → log2_out(s(s(X)), Half, Acc, Y)
U4(X, Half, Acc, Y, log2_out(Half, s(0), s(Acc), Y)) → log2_out(X, s(s(Half)), Acc, Y)
U1(X, Y, log2_out(X, 0, s(0), Y)) → log2_out(X, Y)

The argument filtering Pi contains the following mapping:
log2_in(x1, x2)  =  log2_in(x2)
U1(x1, x2, x3)  =  U1(x3)
log2_in(x1, x2, x3, x4)  =  log2_in(x2, x3, x4)
0  =  0
s(x1)  =  s(x1)
U5(x1, x2, x3, x4)  =  U5(x4)
small_in(x1)  =  small_in
small_out(x1)  =  small_out(x1)
U6(x1, x2, x3, x4)  =  U6(x1, x4)
log2_out(x1, x2, x3, x4)  =  log2_out(x1)
U3(x1, x2, x3, x4, x5)  =  U3(x3, x4, x5)
U4(x1, x2, x3, x4, x5)  =  U4(x1, x5)
U2(x1, x2, x3, x4, x5)  =  U2(x5)
log2_out(x1, x2)  =  log2_out(x1)
SMALL_IN(x1)  =  SMALL_IN
U51(x1, x2, x3, x4)  =  U51(x4)
LOG2_IN(x1, x2, x3, x4)  =  LOG2_IN(x2, x3, x4)
U41(x1, x2, x3, x4, x5)  =  U41(x1, x5)
U31(x1, x2, x3, x4, x5)  =  U31(x3, x4, x5)
LOG2_IN(x1, x2)  =  LOG2_IN(x2)
U21(x1, x2, x3, x4, x5)  =  U21(x5)
U61(x1, x2, x3, x4)  =  U61(x1, x4)
U11(x1, x2, x3)  =  U11(x3)

We have to consider all (P,R,Pi)-chains

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

LOG2_IN(X, Y) → U11(X, Y, log2_in(X, 0, s(0), Y))
LOG2_IN(X, Y) → LOG2_IN(X, 0, s(0), Y)
LOG2_IN(X, Half, Y, Y) → U51(X, Half, Y, small_in(X))
LOG2_IN(X, Half, Y, Y) → SMALL_IN(X)
U51(X, Half, Y, small_out(X)) → U61(X, Half, Y, small_in(Half))
U51(X, Half, Y, small_out(X)) → SMALL_IN(Half)
LOG2_IN(X, s(s(Half)), Acc, Y) → U31(X, Half, Acc, Y, small_in(X))
LOG2_IN(X, s(s(Half)), Acc, Y) → SMALL_IN(X)
U31(X, Half, Acc, Y, small_out(X)) → U41(X, Half, Acc, Y, log2_in(Half, s(0), s(Acc), Y))
U31(X, Half, Acc, Y, small_out(X)) → LOG2_IN(Half, s(0), s(Acc), Y)
LOG2_IN(s(s(X)), Half, Acc, Y) → U21(X, Half, Acc, Y, log2_in(X, s(Half), Acc, Y))
LOG2_IN(s(s(X)), Half, Acc, Y) → LOG2_IN(X, s(Half), Acc, Y)

The TRS R consists of the following rules:

log2_in(X, Y) → U1(X, Y, log2_in(X, 0, s(0), Y))
log2_in(X, Half, Y, Y) → U5(X, Half, Y, small_in(X))
small_in(s(0)) → small_out(s(0))
small_in(0) → small_out(0)
U5(X, Half, Y, small_out(X)) → U6(X, Half, Y, small_in(Half))
U6(X, Half, Y, small_out(Half)) → log2_out(X, Half, Y, Y)
log2_in(X, s(s(Half)), Acc, Y) → U3(X, Half, Acc, Y, small_in(X))
U3(X, Half, Acc, Y, small_out(X)) → U4(X, Half, Acc, Y, log2_in(Half, s(0), s(Acc), Y))
log2_in(s(s(X)), Half, Acc, Y) → U2(X, Half, Acc, Y, log2_in(X, s(Half), Acc, Y))
U2(X, Half, Acc, Y, log2_out(X, s(Half), Acc, Y)) → log2_out(s(s(X)), Half, Acc, Y)
U4(X, Half, Acc, Y, log2_out(Half, s(0), s(Acc), Y)) → log2_out(X, s(s(Half)), Acc, Y)
U1(X, Y, log2_out(X, 0, s(0), Y)) → log2_out(X, Y)

The argument filtering Pi contains the following mapping:
log2_in(x1, x2)  =  log2_in(x2)
U1(x1, x2, x3)  =  U1(x3)
log2_in(x1, x2, x3, x4)  =  log2_in(x2, x3, x4)
0  =  0
s(x1)  =  s(x1)
U5(x1, x2, x3, x4)  =  U5(x4)
small_in(x1)  =  small_in
small_out(x1)  =  small_out(x1)
U6(x1, x2, x3, x4)  =  U6(x1, x4)
log2_out(x1, x2, x3, x4)  =  log2_out(x1)
U3(x1, x2, x3, x4, x5)  =  U3(x3, x4, x5)
U4(x1, x2, x3, x4, x5)  =  U4(x1, x5)
U2(x1, x2, x3, x4, x5)  =  U2(x5)
log2_out(x1, x2)  =  log2_out(x1)
SMALL_IN(x1)  =  SMALL_IN
U51(x1, x2, x3, x4)  =  U51(x4)
LOG2_IN(x1, x2, x3, x4)  =  LOG2_IN(x2, x3, x4)
U41(x1, x2, x3, x4, x5)  =  U41(x1, x5)
U31(x1, x2, x3, x4, x5)  =  U31(x3, x4, x5)
LOG2_IN(x1, x2)  =  LOG2_IN(x2)
U21(x1, x2, x3, x4, x5)  =  U21(x5)
U61(x1, x2, x3, x4)  =  U61(x1, x4)
U11(x1, x2, x3)  =  U11(x3)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 1 SCC with 9 less nodes.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ UsableRulesProof
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

U31(X, Half, Acc, Y, small_out(X)) → LOG2_IN(Half, s(0), s(Acc), Y)
LOG2_IN(X, s(s(Half)), Acc, Y) → U31(X, Half, Acc, Y, small_in(X))
LOG2_IN(s(s(X)), Half, Acc, Y) → LOG2_IN(X, s(Half), Acc, Y)

The TRS R consists of the following rules:

log2_in(X, Y) → U1(X, Y, log2_in(X, 0, s(0), Y))
log2_in(X, Half, Y, Y) → U5(X, Half, Y, small_in(X))
small_in(s(0)) → small_out(s(0))
small_in(0) → small_out(0)
U5(X, Half, Y, small_out(X)) → U6(X, Half, Y, small_in(Half))
U6(X, Half, Y, small_out(Half)) → log2_out(X, Half, Y, Y)
log2_in(X, s(s(Half)), Acc, Y) → U3(X, Half, Acc, Y, small_in(X))
U3(X, Half, Acc, Y, small_out(X)) → U4(X, Half, Acc, Y, log2_in(Half, s(0), s(Acc), Y))
log2_in(s(s(X)), Half, Acc, Y) → U2(X, Half, Acc, Y, log2_in(X, s(Half), Acc, Y))
U2(X, Half, Acc, Y, log2_out(X, s(Half), Acc, Y)) → log2_out(s(s(X)), Half, Acc, Y)
U4(X, Half, Acc, Y, log2_out(Half, s(0), s(Acc), Y)) → log2_out(X, s(s(Half)), Acc, Y)
U1(X, Y, log2_out(X, 0, s(0), Y)) → log2_out(X, Y)

The argument filtering Pi contains the following mapping:
log2_in(x1, x2)  =  log2_in(x2)
U1(x1, x2, x3)  =  U1(x3)
log2_in(x1, x2, x3, x4)  =  log2_in(x2, x3, x4)
0  =  0
s(x1)  =  s(x1)
U5(x1, x2, x3, x4)  =  U5(x4)
small_in(x1)  =  small_in
small_out(x1)  =  small_out(x1)
U6(x1, x2, x3, x4)  =  U6(x1, x4)
log2_out(x1, x2, x3, x4)  =  log2_out(x1)
U3(x1, x2, x3, x4, x5)  =  U3(x3, x4, x5)
U4(x1, x2, x3, x4, x5)  =  U4(x1, x5)
U2(x1, x2, x3, x4, x5)  =  U2(x5)
log2_out(x1, x2)  =  log2_out(x1)
LOG2_IN(x1, x2, x3, x4)  =  LOG2_IN(x2, x3, x4)
U31(x1, x2, x3, x4, x5)  =  U31(x3, x4, x5)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ UsableRulesProof
                ↳ PiDP
                  ↳ PiDPToQDPProof
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

U31(X, Half, Acc, Y, small_out(X)) → LOG2_IN(Half, s(0), s(Acc), Y)
LOG2_IN(X, s(s(Half)), Acc, Y) → U31(X, Half, Acc, Y, small_in(X))
LOG2_IN(s(s(X)), Half, Acc, Y) → LOG2_IN(X, s(Half), Acc, Y)

The TRS R consists of the following rules:

small_in(s(0)) → small_out(s(0))
small_in(0) → small_out(0)

The argument filtering Pi contains the following mapping:
0  =  0
s(x1)  =  s(x1)
small_in(x1)  =  small_in
small_out(x1)  =  small_out(x1)
LOG2_IN(x1, x2, x3, x4)  =  LOG2_IN(x2, x3, x4)
U31(x1, x2, x3, x4, x5)  =  U31(x3, x4, x5)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ UsableRulesProof
                ↳ PiDP
                  ↳ PiDPToQDPProof
                    ↳ QDP
                      ↳ Narrowing
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

LOG2_IN(Half, Acc, Y) → LOG2_IN(s(Half), Acc, Y)
LOG2_IN(s(s(Half)), Acc, Y) → U31(Acc, Y, small_in)
U31(Acc, Y, small_out(X)) → LOG2_IN(s(0), s(Acc), Y)

The TRS R consists of the following rules:

small_in → small_out(s(0))
small_in → small_out(0)

The set Q consists of the following terms:

small_in

We have to consider all (P,Q,R)-chains.
By narrowing [15] the rule LOG2_IN(s(s(Half)), Acc, Y) → U31(Acc, Y, small_in) at position [2] we obtained the following new rules:

LOG2_IN(s(s(y0)), y1, y2) → U31(y1, y2, small_out(0))
LOG2_IN(s(s(y0)), y1, y2) → U31(y1, y2, small_out(s(0)))



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ UsableRulesProof
                ↳ PiDP
                  ↳ PiDPToQDPProof
                    ↳ QDP
                      ↳ Narrowing
                        ↳ QDP
                          ↳ UsableRulesProof
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

LOG2_IN(Half, Acc, Y) → LOG2_IN(s(Half), Acc, Y)
LOG2_IN(s(s(y0)), y1, y2) → U31(y1, y2, small_out(s(0)))
LOG2_IN(s(s(y0)), y1, y2) → U31(y1, y2, small_out(0))
U31(Acc, Y, small_out(X)) → LOG2_IN(s(0), s(Acc), Y)

The TRS R consists of the following rules:

small_in → small_out(s(0))
small_in → small_out(0)

The set Q consists of the following terms:

small_in

We have to consider all (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ UsableRulesProof
                ↳ PiDP
                  ↳ PiDPToQDPProof
                    ↳ QDP
                      ↳ Narrowing
                        ↳ QDP
                          ↳ UsableRulesProof
                            ↳ QDP
                              ↳ QReductionProof
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

LOG2_IN(Half, Acc, Y) → LOG2_IN(s(Half), Acc, Y)
LOG2_IN(s(s(y0)), y1, y2) → U31(y1, y2, small_out(s(0)))
LOG2_IN(s(s(y0)), y1, y2) → U31(y1, y2, small_out(0))
U31(Acc, Y, small_out(X)) → LOG2_IN(s(0), s(Acc), Y)

R is empty.
The set Q consists of the following terms:

small_in

We have to consider all (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

small_in



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ UsableRulesProof
                ↳ PiDP
                  ↳ PiDPToQDPProof
                    ↳ QDP
                      ↳ Narrowing
                        ↳ QDP
                          ↳ UsableRulesProof
                            ↳ QDP
                              ↳ QReductionProof
                                ↳ QDP
                                  ↳ Instantiation
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

LOG2_IN(Half, Acc, Y) → LOG2_IN(s(Half), Acc, Y)
LOG2_IN(s(s(y0)), y1, y2) → U31(y1, y2, small_out(0))
LOG2_IN(s(s(y0)), y1, y2) → U31(y1, y2, small_out(s(0)))
U31(Acc, Y, small_out(X)) → LOG2_IN(s(0), s(Acc), Y)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule LOG2_IN(Half, Acc, Y) → LOG2_IN(s(Half), Acc, Y) we obtained the following new rules:

LOG2_IN(s(0), s(z0), z1) → LOG2_IN(s(s(0)), s(z0), z1)
LOG2_IN(s(z0), z1, z2) → LOG2_IN(s(s(z0)), z1, z2)



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ UsableRulesProof
                ↳ PiDP
                  ↳ PiDPToQDPProof
                    ↳ QDP
                      ↳ Narrowing
                        ↳ QDP
                          ↳ UsableRulesProof
                            ↳ QDP
                              ↳ QReductionProof
                                ↳ QDP
                                  ↳ Instantiation
                                    ↳ QDP
                                      ↳ Instantiation
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

LOG2_IN(s(0), s(z0), z1) → LOG2_IN(s(s(0)), s(z0), z1)
LOG2_IN(s(s(y0)), y1, y2) → U31(y1, y2, small_out(s(0)))
LOG2_IN(s(s(y0)), y1, y2) → U31(y1, y2, small_out(0))
LOG2_IN(s(z0), z1, z2) → LOG2_IN(s(s(z0)), z1, z2)
U31(Acc, Y, small_out(X)) → LOG2_IN(s(0), s(Acc), Y)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule U31(Acc, Y, small_out(X)) → LOG2_IN(s(0), s(Acc), Y) we obtained the following new rules:

U31(z1, z2, small_out(0)) → LOG2_IN(s(0), s(z1), z2)
U31(z1, z2, small_out(s(0))) → LOG2_IN(s(0), s(z1), z2)



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ UsableRulesProof
                ↳ PiDP
                  ↳ PiDPToQDPProof
                    ↳ QDP
                      ↳ Narrowing
                        ↳ QDP
                          ↳ UsableRulesProof
                            ↳ QDP
                              ↳ QReductionProof
                                ↳ QDP
                                  ↳ Instantiation
                                    ↳ QDP
                                      ↳ Instantiation
                                        ↳ QDP
                                          ↳ Instantiation
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U31(z1, z2, small_out(0)) → LOG2_IN(s(0), s(z1), z2)
LOG2_IN(s(0), s(z0), z1) → LOG2_IN(s(s(0)), s(z0), z1)
LOG2_IN(s(s(y0)), y1, y2) → U31(y1, y2, small_out(0))
LOG2_IN(s(s(y0)), y1, y2) → U31(y1, y2, small_out(s(0)))
U31(z1, z2, small_out(s(0))) → LOG2_IN(s(0), s(z1), z2)
LOG2_IN(s(z0), z1, z2) → LOG2_IN(s(s(z0)), z1, z2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule LOG2_IN(s(z0), z1, z2) → LOG2_IN(s(s(z0)), z1, z2) we obtained the following new rules:

LOG2_IN(s(s(z0)), z1, z2) → LOG2_IN(s(s(s(z0))), z1, z2)
LOG2_IN(s(0), s(z0), z1) → LOG2_IN(s(s(0)), s(z0), z1)
LOG2_IN(s(s(0)), s(z0), z1) → LOG2_IN(s(s(s(0))), s(z0), z1)



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ UsableRulesProof
                ↳ PiDP
                  ↳ PiDPToQDPProof
                    ↳ QDP
                      ↳ Narrowing
                        ↳ QDP
                          ↳ UsableRulesProof
                            ↳ QDP
                              ↳ QReductionProof
                                ↳ QDP
                                  ↳ Instantiation
                                    ↳ QDP
                                      ↳ Instantiation
                                        ↳ QDP
                                          ↳ Instantiation
                                            ↳ QDP
                                              ↳ Instantiation
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

LOG2_IN(s(s(z0)), z1, z2) → LOG2_IN(s(s(s(z0))), z1, z2)
U31(z1, z2, small_out(0)) → LOG2_IN(s(0), s(z1), z2)
LOG2_IN(s(0), s(z0), z1) → LOG2_IN(s(s(0)), s(z0), z1)
LOG2_IN(s(s(0)), s(z0), z1) → LOG2_IN(s(s(s(0))), s(z0), z1)
LOG2_IN(s(s(y0)), y1, y2) → U31(y1, y2, small_out(s(0)))
LOG2_IN(s(s(y0)), y1, y2) → U31(y1, y2, small_out(0))
U31(z1, z2, small_out(s(0))) → LOG2_IN(s(0), s(z1), z2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule LOG2_IN(s(s(y0)), y1, y2) → U31(y1, y2, small_out(s(0))) we obtained the following new rules:

LOG2_IN(s(s(s(0))), s(z0), z1) → U31(s(z0), z1, small_out(s(0)))
LOG2_IN(s(s(s(z0))), z1, z2) → U31(z1, z2, small_out(s(0)))
LOG2_IN(s(s(0)), s(z0), z1) → U31(s(z0), z1, small_out(s(0)))



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ UsableRulesProof
                ↳ PiDP
                  ↳ PiDPToQDPProof
                    ↳ QDP
                      ↳ Narrowing
                        ↳ QDP
                          ↳ UsableRulesProof
                            ↳ QDP
                              ↳ QReductionProof
                                ↳ QDP
                                  ↳ Instantiation
                                    ↳ QDP
                                      ↳ Instantiation
                                        ↳ QDP
                                          ↳ Instantiation
                                            ↳ QDP
                                              ↳ Instantiation
                                                ↳ QDP
                                                  ↳ Instantiation
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

LOG2_IN(s(s(s(0))), s(z0), z1) → U31(s(z0), z1, small_out(s(0)))
U31(z1, z2, small_out(0)) → LOG2_IN(s(0), s(z1), z2)
LOG2_IN(s(s(z0)), z1, z2) → LOG2_IN(s(s(s(z0))), z1, z2)
LOG2_IN(s(0), s(z0), z1) → LOG2_IN(s(s(0)), s(z0), z1)
LOG2_IN(s(s(0)), s(z0), z1) → LOG2_IN(s(s(s(0))), s(z0), z1)
LOG2_IN(s(s(s(z0))), z1, z2) → U31(z1, z2, small_out(s(0)))
LOG2_IN(s(s(y0)), y1, y2) → U31(y1, y2, small_out(0))
U31(z1, z2, small_out(s(0))) → LOG2_IN(s(0), s(z1), z2)
LOG2_IN(s(s(0)), s(z0), z1) → U31(s(z0), z1, small_out(s(0)))

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule LOG2_IN(s(s(y0)), y1, y2) → U31(y1, y2, small_out(0)) we obtained the following new rules:

LOG2_IN(s(s(s(z0))), z1, z2) → U31(z1, z2, small_out(0))
LOG2_IN(s(s(s(0))), s(z0), z1) → U31(s(z0), z1, small_out(0))
LOG2_IN(s(s(0)), s(z0), z1) → U31(s(z0), z1, small_out(0))



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ UsableRulesProof
                ↳ PiDP
                  ↳ PiDPToQDPProof
                    ↳ QDP
                      ↳ Narrowing
                        ↳ QDP
                          ↳ UsableRulesProof
                            ↳ QDP
                              ↳ QReductionProof
                                ↳ QDP
                                  ↳ Instantiation
                                    ↳ QDP
                                      ↳ Instantiation
                                        ↳ QDP
                                          ↳ Instantiation
                                            ↳ QDP
                                              ↳ Instantiation
                                                ↳ QDP
                                                  ↳ Instantiation
                                                    ↳ QDP
                                                      ↳ NonTerminationProof
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

LOG2_IN(s(s(s(0))), s(z0), z1) → U31(s(z0), z1, small_out(s(0)))
LOG2_IN(s(s(z0)), z1, z2) → LOG2_IN(s(s(s(z0))), z1, z2)
U31(z1, z2, small_out(0)) → LOG2_IN(s(0), s(z1), z2)
LOG2_IN(s(0), s(z0), z1) → LOG2_IN(s(s(0)), s(z0), z1)
LOG2_IN(s(s(0)), s(z0), z1) → LOG2_IN(s(s(s(0))), s(z0), z1)
LOG2_IN(s(s(s(z0))), z1, z2) → U31(z1, z2, small_out(s(0)))
LOG2_IN(s(s(s(z0))), z1, z2) → U31(z1, z2, small_out(0))
U31(z1, z2, small_out(s(0))) → LOG2_IN(s(0), s(z1), z2)
LOG2_IN(s(s(s(0))), s(z0), z1) → U31(s(z0), z1, small_out(0))
LOG2_IN(s(s(0)), s(z0), z1) → U31(s(z0), z1, small_out(0))
LOG2_IN(s(s(0)), s(z0), z1) → U31(s(z0), z1, small_out(s(0)))

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

The TRS P consists of the following rules:

LOG2_IN(s(s(s(0))), s(z0), z1) → U31(s(z0), z1, small_out(s(0)))
LOG2_IN(s(s(z0)), z1, z2) → LOG2_IN(s(s(s(z0))), z1, z2)
U31(z1, z2, small_out(0)) → LOG2_IN(s(0), s(z1), z2)
LOG2_IN(s(0), s(z0), z1) → LOG2_IN(s(s(0)), s(z0), z1)
LOG2_IN(s(s(0)), s(z0), z1) → LOG2_IN(s(s(s(0))), s(z0), z1)
LOG2_IN(s(s(s(z0))), z1, z2) → U31(z1, z2, small_out(s(0)))
LOG2_IN(s(s(s(z0))), z1, z2) → U31(z1, z2, small_out(0))
U31(z1, z2, small_out(s(0))) → LOG2_IN(s(0), s(z1), z2)
LOG2_IN(s(s(s(0))), s(z0), z1) → U31(s(z0), z1, small_out(0))
LOG2_IN(s(s(0)), s(z0), z1) → U31(s(z0), z1, small_out(0))
LOG2_IN(s(s(0)), s(z0), z1) → U31(s(z0), z1, small_out(s(0)))

The TRS R consists of the following rules:none


s = LOG2_IN(s(s(z0)), z1, z2) evaluates to t =LOG2_IN(s(s(s(z0))), z1, z2)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:



Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from LOG2_IN(s(s(z0)), z1, z2) to LOG2_IN(s(s(s(z0))), z1, z2).




We use the technique of [30].Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

log2_in(X, Y) → U1(X, Y, log2_in(X, 0, s(0), Y))
log2_in(X, Half, Y, Y) → U5(X, Half, Y, small_in(X))
small_in(s(0)) → small_out(s(0))
small_in(0) → small_out(0)
U5(X, Half, Y, small_out(X)) → U6(X, Half, Y, small_in(Half))
U6(X, Half, Y, small_out(Half)) → log2_out(X, Half, Y, Y)
log2_in(X, s(s(Half)), Acc, Y) → U3(X, Half, Acc, Y, small_in(X))
U3(X, Half, Acc, Y, small_out(X)) → U4(X, Half, Acc, Y, log2_in(Half, s(0), s(Acc), Y))
log2_in(s(s(X)), Half, Acc, Y) → U2(X, Half, Acc, Y, log2_in(X, s(Half), Acc, Y))
U2(X, Half, Acc, Y, log2_out(X, s(Half), Acc, Y)) → log2_out(s(s(X)), Half, Acc, Y)
U4(X, Half, Acc, Y, log2_out(Half, s(0), s(Acc), Y)) → log2_out(X, s(s(Half)), Acc, Y)
U1(X, Y, log2_out(X, 0, s(0), Y)) → log2_out(X, Y)

The argument filtering Pi contains the following mapping:
log2_in(x1, x2)  =  log2_in(x2)
U1(x1, x2, x3)  =  U1(x2, x3)
log2_in(x1, x2, x3, x4)  =  log2_in(x2, x3, x4)
0  =  0
s(x1)  =  s(x1)
U5(x1, x2, x3, x4)  =  U5(x2, x3, x4)
small_in(x1)  =  small_in
small_out(x1)  =  small_out(x1)
U6(x1, x2, x3, x4)  =  U6(x1, x2, x3, x4)
log2_out(x1, x2, x3, x4)  =  log2_out(x1, x2, x3, x4)
U3(x1, x2, x3, x4, x5)  =  U3(x2, x3, x4, x5)
U4(x1, x2, x3, x4, x5)  =  U4(x1, x2, x3, x4, x5)
U2(x1, x2, x3, x4, x5)  =  U2(x2, x3, x4, x5)
log2_out(x1, x2)  =  log2_out(x1, x2)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

log2_in(X, Y) → U1(X, Y, log2_in(X, 0, s(0), Y))
log2_in(X, Half, Y, Y) → U5(X, Half, Y, small_in(X))
small_in(s(0)) → small_out(s(0))
small_in(0) → small_out(0)
U5(X, Half, Y, small_out(X)) → U6(X, Half, Y, small_in(Half))
U6(X, Half, Y, small_out(Half)) → log2_out(X, Half, Y, Y)
log2_in(X, s(s(Half)), Acc, Y) → U3(X, Half, Acc, Y, small_in(X))
U3(X, Half, Acc, Y, small_out(X)) → U4(X, Half, Acc, Y, log2_in(Half, s(0), s(Acc), Y))
log2_in(s(s(X)), Half, Acc, Y) → U2(X, Half, Acc, Y, log2_in(X, s(Half), Acc, Y))
U2(X, Half, Acc, Y, log2_out(X, s(Half), Acc, Y)) → log2_out(s(s(X)), Half, Acc, Y)
U4(X, Half, Acc, Y, log2_out(Half, s(0), s(Acc), Y)) → log2_out(X, s(s(Half)), Acc, Y)
U1(X, Y, log2_out(X, 0, s(0), Y)) → log2_out(X, Y)

The argument filtering Pi contains the following mapping:
log2_in(x1, x2)  =  log2_in(x2)
U1(x1, x2, x3)  =  U1(x2, x3)
log2_in(x1, x2, x3, x4)  =  log2_in(x2, x3, x4)
0  =  0
s(x1)  =  s(x1)
U5(x1, x2, x3, x4)  =  U5(x2, x3, x4)
small_in(x1)  =  small_in
small_out(x1)  =  small_out(x1)
U6(x1, x2, x3, x4)  =  U6(x1, x2, x3, x4)
log2_out(x1, x2, x3, x4)  =  log2_out(x1, x2, x3, x4)
U3(x1, x2, x3, x4, x5)  =  U3(x2, x3, x4, x5)
U4(x1, x2, x3, x4, x5)  =  U4(x1, x2, x3, x4, x5)
U2(x1, x2, x3, x4, x5)  =  U2(x2, x3, x4, x5)
log2_out(x1, x2)  =  log2_out(x1, x2)


Using Dependency Pairs [1,30] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

LOG2_IN(X, Y) → U11(X, Y, log2_in(X, 0, s(0), Y))
LOG2_IN(X, Y) → LOG2_IN(X, 0, s(0), Y)
LOG2_IN(X, Half, Y, Y) → U51(X, Half, Y, small_in(X))
LOG2_IN(X, Half, Y, Y) → SMALL_IN(X)
U51(X, Half, Y, small_out(X)) → U61(X, Half, Y, small_in(Half))
U51(X, Half, Y, small_out(X)) → SMALL_IN(Half)
LOG2_IN(X, s(s(Half)), Acc, Y) → U31(X, Half, Acc, Y, small_in(X))
LOG2_IN(X, s(s(Half)), Acc, Y) → SMALL_IN(X)
U31(X, Half, Acc, Y, small_out(X)) → U41(X, Half, Acc, Y, log2_in(Half, s(0), s(Acc), Y))
U31(X, Half, Acc, Y, small_out(X)) → LOG2_IN(Half, s(0), s(Acc), Y)
LOG2_IN(s(s(X)), Half, Acc, Y) → U21(X, Half, Acc, Y, log2_in(X, s(Half), Acc, Y))
LOG2_IN(s(s(X)), Half, Acc, Y) → LOG2_IN(X, s(Half), Acc, Y)

The TRS R consists of the following rules:

log2_in(X, Y) → U1(X, Y, log2_in(X, 0, s(0), Y))
log2_in(X, Half, Y, Y) → U5(X, Half, Y, small_in(X))
small_in(s(0)) → small_out(s(0))
small_in(0) → small_out(0)
U5(X, Half, Y, small_out(X)) → U6(X, Half, Y, small_in(Half))
U6(X, Half, Y, small_out(Half)) → log2_out(X, Half, Y, Y)
log2_in(X, s(s(Half)), Acc, Y) → U3(X, Half, Acc, Y, small_in(X))
U3(X, Half, Acc, Y, small_out(X)) → U4(X, Half, Acc, Y, log2_in(Half, s(0), s(Acc), Y))
log2_in(s(s(X)), Half, Acc, Y) → U2(X, Half, Acc, Y, log2_in(X, s(Half), Acc, Y))
U2(X, Half, Acc, Y, log2_out(X, s(Half), Acc, Y)) → log2_out(s(s(X)), Half, Acc, Y)
U4(X, Half, Acc, Y, log2_out(Half, s(0), s(Acc), Y)) → log2_out(X, s(s(Half)), Acc, Y)
U1(X, Y, log2_out(X, 0, s(0), Y)) → log2_out(X, Y)

The argument filtering Pi contains the following mapping:
log2_in(x1, x2)  =  log2_in(x2)
U1(x1, x2, x3)  =  U1(x2, x3)
log2_in(x1, x2, x3, x4)  =  log2_in(x2, x3, x4)
0  =  0
s(x1)  =  s(x1)
U5(x1, x2, x3, x4)  =  U5(x2, x3, x4)
small_in(x1)  =  small_in
small_out(x1)  =  small_out(x1)
U6(x1, x2, x3, x4)  =  U6(x1, x2, x3, x4)
log2_out(x1, x2, x3, x4)  =  log2_out(x1, x2, x3, x4)
U3(x1, x2, x3, x4, x5)  =  U3(x2, x3, x4, x5)
U4(x1, x2, x3, x4, x5)  =  U4(x1, x2, x3, x4, x5)
U2(x1, x2, x3, x4, x5)  =  U2(x2, x3, x4, x5)
log2_out(x1, x2)  =  log2_out(x1, x2)
SMALL_IN(x1)  =  SMALL_IN
U51(x1, x2, x3, x4)  =  U51(x2, x3, x4)
LOG2_IN(x1, x2, x3, x4)  =  LOG2_IN(x2, x3, x4)
U41(x1, x2, x3, x4, x5)  =  U41(x1, x2, x3, x4, x5)
U31(x1, x2, x3, x4, x5)  =  U31(x2, x3, x4, x5)
LOG2_IN(x1, x2)  =  LOG2_IN(x2)
U21(x1, x2, x3, x4, x5)  =  U21(x2, x3, x4, x5)
U61(x1, x2, x3, x4)  =  U61(x1, x2, x3, x4)
U11(x1, x2, x3)  =  U11(x2, x3)

We have to consider all (P,R,Pi)-chains

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

LOG2_IN(X, Y) → U11(X, Y, log2_in(X, 0, s(0), Y))
LOG2_IN(X, Y) → LOG2_IN(X, 0, s(0), Y)
LOG2_IN(X, Half, Y, Y) → U51(X, Half, Y, small_in(X))
LOG2_IN(X, Half, Y, Y) → SMALL_IN(X)
U51(X, Half, Y, small_out(X)) → U61(X, Half, Y, small_in(Half))
U51(X, Half, Y, small_out(X)) → SMALL_IN(Half)
LOG2_IN(X, s(s(Half)), Acc, Y) → U31(X, Half, Acc, Y, small_in(X))
LOG2_IN(X, s(s(Half)), Acc, Y) → SMALL_IN(X)
U31(X, Half, Acc, Y, small_out(X)) → U41(X, Half, Acc, Y, log2_in(Half, s(0), s(Acc), Y))
U31(X, Half, Acc, Y, small_out(X)) → LOG2_IN(Half, s(0), s(Acc), Y)
LOG2_IN(s(s(X)), Half, Acc, Y) → U21(X, Half, Acc, Y, log2_in(X, s(Half), Acc, Y))
LOG2_IN(s(s(X)), Half, Acc, Y) → LOG2_IN(X, s(Half), Acc, Y)

The TRS R consists of the following rules:

log2_in(X, Y) → U1(X, Y, log2_in(X, 0, s(0), Y))
log2_in(X, Half, Y, Y) → U5(X, Half, Y, small_in(X))
small_in(s(0)) → small_out(s(0))
small_in(0) → small_out(0)
U5(X, Half, Y, small_out(X)) → U6(X, Half, Y, small_in(Half))
U6(X, Half, Y, small_out(Half)) → log2_out(X, Half, Y, Y)
log2_in(X, s(s(Half)), Acc, Y) → U3(X, Half, Acc, Y, small_in(X))
U3(X, Half, Acc, Y, small_out(X)) → U4(X, Half, Acc, Y, log2_in(Half, s(0), s(Acc), Y))
log2_in(s(s(X)), Half, Acc, Y) → U2(X, Half, Acc, Y, log2_in(X, s(Half), Acc, Y))
U2(X, Half, Acc, Y, log2_out(X, s(Half), Acc, Y)) → log2_out(s(s(X)), Half, Acc, Y)
U4(X, Half, Acc, Y, log2_out(Half, s(0), s(Acc), Y)) → log2_out(X, s(s(Half)), Acc, Y)
U1(X, Y, log2_out(X, 0, s(0), Y)) → log2_out(X, Y)

The argument filtering Pi contains the following mapping:
log2_in(x1, x2)  =  log2_in(x2)
U1(x1, x2, x3)  =  U1(x2, x3)
log2_in(x1, x2, x3, x4)  =  log2_in(x2, x3, x4)
0  =  0
s(x1)  =  s(x1)
U5(x1, x2, x3, x4)  =  U5(x2, x3, x4)
small_in(x1)  =  small_in
small_out(x1)  =  small_out(x1)
U6(x1, x2, x3, x4)  =  U6(x1, x2, x3, x4)
log2_out(x1, x2, x3, x4)  =  log2_out(x1, x2, x3, x4)
U3(x1, x2, x3, x4, x5)  =  U3(x2, x3, x4, x5)
U4(x1, x2, x3, x4, x5)  =  U4(x1, x2, x3, x4, x5)
U2(x1, x2, x3, x4, x5)  =  U2(x2, x3, x4, x5)
log2_out(x1, x2)  =  log2_out(x1, x2)
SMALL_IN(x1)  =  SMALL_IN
U51(x1, x2, x3, x4)  =  U51(x2, x3, x4)
LOG2_IN(x1, x2, x3, x4)  =  LOG2_IN(x2, x3, x4)
U41(x1, x2, x3, x4, x5)  =  U41(x1, x2, x3, x4, x5)
U31(x1, x2, x3, x4, x5)  =  U31(x2, x3, x4, x5)
LOG2_IN(x1, x2)  =  LOG2_IN(x2)
U21(x1, x2, x3, x4, x5)  =  U21(x2, x3, x4, x5)
U61(x1, x2, x3, x4)  =  U61(x1, x2, x3, x4)
U11(x1, x2, x3)  =  U11(x2, x3)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 1 SCC with 9 less nodes.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ UsableRulesProof

Pi DP problem:
The TRS P consists of the following rules:

U31(X, Half, Acc, Y, small_out(X)) → LOG2_IN(Half, s(0), s(Acc), Y)
LOG2_IN(X, s(s(Half)), Acc, Y) → U31(X, Half, Acc, Y, small_in(X))
LOG2_IN(s(s(X)), Half, Acc, Y) → LOG2_IN(X, s(Half), Acc, Y)

The TRS R consists of the following rules:

log2_in(X, Y) → U1(X, Y, log2_in(X, 0, s(0), Y))
log2_in(X, Half, Y, Y) → U5(X, Half, Y, small_in(X))
small_in(s(0)) → small_out(s(0))
small_in(0) → small_out(0)
U5(X, Half, Y, small_out(X)) → U6(X, Half, Y, small_in(Half))
U6(X, Half, Y, small_out(Half)) → log2_out(X, Half, Y, Y)
log2_in(X, s(s(Half)), Acc, Y) → U3(X, Half, Acc, Y, small_in(X))
U3(X, Half, Acc, Y, small_out(X)) → U4(X, Half, Acc, Y, log2_in(Half, s(0), s(Acc), Y))
log2_in(s(s(X)), Half, Acc, Y) → U2(X, Half, Acc, Y, log2_in(X, s(Half), Acc, Y))
U2(X, Half, Acc, Y, log2_out(X, s(Half), Acc, Y)) → log2_out(s(s(X)), Half, Acc, Y)
U4(X, Half, Acc, Y, log2_out(Half, s(0), s(Acc), Y)) → log2_out(X, s(s(Half)), Acc, Y)
U1(X, Y, log2_out(X, 0, s(0), Y)) → log2_out(X, Y)

The argument filtering Pi contains the following mapping:
log2_in(x1, x2)  =  log2_in(x2)
U1(x1, x2, x3)  =  U1(x2, x3)
log2_in(x1, x2, x3, x4)  =  log2_in(x2, x3, x4)
0  =  0
s(x1)  =  s(x1)
U5(x1, x2, x3, x4)  =  U5(x2, x3, x4)
small_in(x1)  =  small_in
small_out(x1)  =  small_out(x1)
U6(x1, x2, x3, x4)  =  U6(x1, x2, x3, x4)
log2_out(x1, x2, x3, x4)  =  log2_out(x1, x2, x3, x4)
U3(x1, x2, x3, x4, x5)  =  U3(x2, x3, x4, x5)
U4(x1, x2, x3, x4, x5)  =  U4(x1, x2, x3, x4, x5)
U2(x1, x2, x3, x4, x5)  =  U2(x2, x3, x4, x5)
log2_out(x1, x2)  =  log2_out(x1, x2)
LOG2_IN(x1, x2, x3, x4)  =  LOG2_IN(x2, x3, x4)
U31(x1, x2, x3, x4, x5)  =  U31(x2, x3, x4, x5)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ UsableRulesProof
                ↳ PiDP
                  ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

U31(X, Half, Acc, Y, small_out(X)) → LOG2_IN(Half, s(0), s(Acc), Y)
LOG2_IN(X, s(s(Half)), Acc, Y) → U31(X, Half, Acc, Y, small_in(X))
LOG2_IN(s(s(X)), Half, Acc, Y) → LOG2_IN(X, s(Half), Acc, Y)

The TRS R consists of the following rules:

small_in(s(0)) → small_out(s(0))
small_in(0) → small_out(0)

The argument filtering Pi contains the following mapping:
0  =  0
s(x1)  =  s(x1)
small_in(x1)  =  small_in
small_out(x1)  =  small_out(x1)
LOG2_IN(x1, x2, x3, x4)  =  LOG2_IN(x2, x3, x4)
U31(x1, x2, x3, x4, x5)  =  U31(x2, x3, x4, x5)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ UsableRulesProof
                ↳ PiDP
                  ↳ PiDPToQDPProof
                    ↳ QDP
                      ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

LOG2_IN(s(s(Half)), Acc, Y) → U31(Half, Acc, Y, small_in)
LOG2_IN(Half, Acc, Y) → LOG2_IN(s(Half), Acc, Y)
U31(Half, Acc, Y, small_out(X)) → LOG2_IN(s(0), s(Acc), Y)

The TRS R consists of the following rules:

small_in → small_out(s(0))
small_in → small_out(0)

The set Q consists of the following terms:

small_in

We have to consider all (P,Q,R)-chains.
By narrowing [15] the rule LOG2_IN(s(s(Half)), Acc, Y) → U31(Half, Acc, Y, small_in) at position [3] we obtained the following new rules:

LOG2_IN(s(s(y0)), y1, y2) → U31(y0, y1, y2, small_out(0))
LOG2_IN(s(s(y0)), y1, y2) → U31(y0, y1, y2, small_out(s(0)))



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ UsableRulesProof
                ↳ PiDP
                  ↳ PiDPToQDPProof
                    ↳ QDP
                      ↳ Narrowing
                        ↳ QDP
                          ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

LOG2_IN(s(s(y0)), y1, y2) → U31(y0, y1, y2, small_out(0))
U31(Half, Acc, Y, small_out(X)) → LOG2_IN(s(0), s(Acc), Y)
LOG2_IN(Half, Acc, Y) → LOG2_IN(s(Half), Acc, Y)
LOG2_IN(s(s(y0)), y1, y2) → U31(y0, y1, y2, small_out(s(0)))

The TRS R consists of the following rules:

small_in → small_out(s(0))
small_in → small_out(0)

The set Q consists of the following terms:

small_in

We have to consider all (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ UsableRulesProof
                ↳ PiDP
                  ↳ PiDPToQDPProof
                    ↳ QDP
                      ↳ Narrowing
                        ↳ QDP
                          ↳ UsableRulesProof
                            ↳ QDP
                              ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

LOG2_IN(s(s(y0)), y1, y2) → U31(y0, y1, y2, small_out(0))
LOG2_IN(Half, Acc, Y) → LOG2_IN(s(Half), Acc, Y)
U31(Half, Acc, Y, small_out(X)) → LOG2_IN(s(0), s(Acc), Y)
LOG2_IN(s(s(y0)), y1, y2) → U31(y0, y1, y2, small_out(s(0)))

R is empty.
The set Q consists of the following terms:

small_in

We have to consider all (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

small_in



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ UsableRulesProof
                ↳ PiDP
                  ↳ PiDPToQDPProof
                    ↳ QDP
                      ↳ Narrowing
                        ↳ QDP
                          ↳ UsableRulesProof
                            ↳ QDP
                              ↳ QReductionProof
                                ↳ QDP
                                  ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

LOG2_IN(s(s(y0)), y1, y2) → U31(y0, y1, y2, small_out(0))
U31(Half, Acc, Y, small_out(X)) → LOG2_IN(s(0), s(Acc), Y)
LOG2_IN(Half, Acc, Y) → LOG2_IN(s(Half), Acc, Y)
LOG2_IN(s(s(y0)), y1, y2) → U31(y0, y1, y2, small_out(s(0)))

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule LOG2_IN(Half, Acc, Y) → LOG2_IN(s(Half), Acc, Y) we obtained the following new rules:

LOG2_IN(s(0), s(z1), z2) → LOG2_IN(s(s(0)), s(z1), z2)
LOG2_IN(s(z0), z1, z2) → LOG2_IN(s(s(z0)), z1, z2)



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ UsableRulesProof
                ↳ PiDP
                  ↳ PiDPToQDPProof
                    ↳ QDP
                      ↳ Narrowing
                        ↳ QDP
                          ↳ UsableRulesProof
                            ↳ QDP
                              ↳ QReductionProof
                                ↳ QDP
                                  ↳ Instantiation
                                    ↳ QDP
                                      ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

LOG2_IN(s(s(y0)), y1, y2) → U31(y0, y1, y2, small_out(0))
LOG2_IN(s(0), s(z1), z2) → LOG2_IN(s(s(0)), s(z1), z2)
U31(Half, Acc, Y, small_out(X)) → LOG2_IN(s(0), s(Acc), Y)
LOG2_IN(s(z0), z1, z2) → LOG2_IN(s(s(z0)), z1, z2)
LOG2_IN(s(s(y0)), y1, y2) → U31(y0, y1, y2, small_out(s(0)))

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule U31(Half, Acc, Y, small_out(X)) → LOG2_IN(s(0), s(Acc), Y) we obtained the following new rules:

U31(z0, z1, z2, small_out(0)) → LOG2_IN(s(0), s(z1), z2)
U31(z0, z1, z2, small_out(s(0))) → LOG2_IN(s(0), s(z1), z2)



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ UsableRulesProof
                ↳ PiDP
                  ↳ PiDPToQDPProof
                    ↳ QDP
                      ↳ Narrowing
                        ↳ QDP
                          ↳ UsableRulesProof
                            ↳ QDP
                              ↳ QReductionProof
                                ↳ QDP
                                  ↳ Instantiation
                                    ↳ QDP
                                      ↳ Instantiation
                                        ↳ QDP
                                          ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

U31(z0, z1, z2, small_out(0)) → LOG2_IN(s(0), s(z1), z2)
LOG2_IN(s(s(y0)), y1, y2) → U31(y0, y1, y2, small_out(0))
LOG2_IN(s(0), s(z1), z2) → LOG2_IN(s(s(0)), s(z1), z2)
U31(z0, z1, z2, small_out(s(0))) → LOG2_IN(s(0), s(z1), z2)
LOG2_IN(s(s(y0)), y1, y2) → U31(y0, y1, y2, small_out(s(0)))
LOG2_IN(s(z0), z1, z2) → LOG2_IN(s(s(z0)), z1, z2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule LOG2_IN(s(z0), z1, z2) → LOG2_IN(s(s(z0)), z1, z2) we obtained the following new rules:

LOG2_IN(s(s(z0)), z1, z2) → LOG2_IN(s(s(s(z0))), z1, z2)
LOG2_IN(s(0), s(z1), z2) → LOG2_IN(s(s(0)), s(z1), z2)
LOG2_IN(s(s(0)), s(z0), z1) → LOG2_IN(s(s(s(0))), s(z0), z1)



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ UsableRulesProof
                ↳ PiDP
                  ↳ PiDPToQDPProof
                    ↳ QDP
                      ↳ Narrowing
                        ↳ QDP
                          ↳ UsableRulesProof
                            ↳ QDP
                              ↳ QReductionProof
                                ↳ QDP
                                  ↳ Instantiation
                                    ↳ QDP
                                      ↳ Instantiation
                                        ↳ QDP
                                          ↳ Instantiation
                                            ↳ QDP
                                              ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

LOG2_IN(s(s(z0)), z1, z2) → LOG2_IN(s(s(s(z0))), z1, z2)
LOG2_IN(s(s(y0)), y1, y2) → U31(y0, y1, y2, small_out(0))
U31(z0, z1, z2, small_out(0)) → LOG2_IN(s(0), s(z1), z2)
LOG2_IN(s(0), s(z1), z2) → LOG2_IN(s(s(0)), s(z1), z2)
LOG2_IN(s(s(0)), s(z0), z1) → LOG2_IN(s(s(s(0))), s(z0), z1)
U31(z0, z1, z2, small_out(s(0))) → LOG2_IN(s(0), s(z1), z2)
LOG2_IN(s(s(y0)), y1, y2) → U31(y0, y1, y2, small_out(s(0)))

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule LOG2_IN(s(s(y0)), y1, y2) → U31(y0, y1, y2, small_out(0)) we obtained the following new rules:

LOG2_IN(s(s(s(0))), s(z0), z1) → U31(s(0), s(z0), z1, small_out(0))
LOG2_IN(s(s(s(z0))), z1, z2) → U31(s(z0), z1, z2, small_out(0))
LOG2_IN(s(s(0)), s(z0), z1) → U31(0, s(z0), z1, small_out(0))



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ UsableRulesProof
                ↳ PiDP
                  ↳ PiDPToQDPProof
                    ↳ QDP
                      ↳ Narrowing
                        ↳ QDP
                          ↳ UsableRulesProof
                            ↳ QDP
                              ↳ QReductionProof
                                ↳ QDP
                                  ↳ Instantiation
                                    ↳ QDP
                                      ↳ Instantiation
                                        ↳ QDP
                                          ↳ Instantiation
                                            ↳ QDP
                                              ↳ Instantiation
                                                ↳ QDP
                                                  ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

U31(z0, z1, z2, small_out(0)) → LOG2_IN(s(0), s(z1), z2)
LOG2_IN(s(s(z0)), z1, z2) → LOG2_IN(s(s(s(z0))), z1, z2)
LOG2_IN(s(0), s(z1), z2) → LOG2_IN(s(s(0)), s(z1), z2)
U31(z0, z1, z2, small_out(s(0))) → LOG2_IN(s(0), s(z1), z2)
LOG2_IN(s(s(0)), s(z0), z1) → LOG2_IN(s(s(s(0))), s(z0), z1)
LOG2_IN(s(s(s(0))), s(z0), z1) → U31(s(0), s(z0), z1, small_out(0))
LOG2_IN(s(s(s(z0))), z1, z2) → U31(s(z0), z1, z2, small_out(0))
LOG2_IN(s(s(0)), s(z0), z1) → U31(0, s(z0), z1, small_out(0))
LOG2_IN(s(s(y0)), y1, y2) → U31(y0, y1, y2, small_out(s(0)))

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule LOG2_IN(s(s(y0)), y1, y2) → U31(y0, y1, y2, small_out(s(0))) we obtained the following new rules:

LOG2_IN(s(s(0)), s(z0), z1) → U31(0, s(z0), z1, small_out(s(0)))
LOG2_IN(s(s(s(0))), s(z0), z1) → U31(s(0), s(z0), z1, small_out(s(0)))
LOG2_IN(s(s(s(z0))), z1, z2) → U31(s(z0), z1, z2, small_out(s(0)))



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ UsableRulesProof
                ↳ PiDP
                  ↳ PiDPToQDPProof
                    ↳ QDP
                      ↳ Narrowing
                        ↳ QDP
                          ↳ UsableRulesProof
                            ↳ QDP
                              ↳ QReductionProof
                                ↳ QDP
                                  ↳ Instantiation
                                    ↳ QDP
                                      ↳ Instantiation
                                        ↳ QDP
                                          ↳ Instantiation
                                            ↳ QDP
                                              ↳ Instantiation
                                                ↳ QDP
                                                  ↳ Instantiation
                                                    ↳ QDP
                                                      ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

LOG2_IN(s(s(z0)), z1, z2) → LOG2_IN(s(s(s(z0))), z1, z2)
U31(z0, z1, z2, small_out(0)) → LOG2_IN(s(0), s(z1), z2)
LOG2_IN(s(0), s(z1), z2) → LOG2_IN(s(s(0)), s(z1), z2)
LOG2_IN(s(s(0)), s(z0), z1) → LOG2_IN(s(s(s(0))), s(z0), z1)
U31(z0, z1, z2, small_out(s(0))) → LOG2_IN(s(0), s(z1), z2)
LOG2_IN(s(s(0)), s(z0), z1) → U31(0, s(z0), z1, small_out(s(0)))
LOG2_IN(s(s(s(0))), s(z0), z1) → U31(s(0), s(z0), z1, small_out(0))
LOG2_IN(s(s(s(z0))), z1, z2) → U31(s(z0), z1, z2, small_out(0))
LOG2_IN(s(s(0)), s(z0), z1) → U31(0, s(z0), z1, small_out(0))
LOG2_IN(s(s(s(0))), s(z0), z1) → U31(s(0), s(z0), z1, small_out(s(0)))
LOG2_IN(s(s(s(z0))), z1, z2) → U31(s(z0), z1, z2, small_out(s(0)))

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule U31(z0, z1, z2, small_out(0)) → LOG2_IN(s(0), s(z1), z2) we obtained the following new rules:

U31(s(0), s(z0), z1, small_out(0)) → LOG2_IN(s(0), s(s(z0)), z1)
U31(0, s(z0), z1, small_out(0)) → LOG2_IN(s(0), s(s(z0)), z1)
U31(s(z0), z1, z2, small_out(0)) → LOG2_IN(s(0), s(z1), z2)



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ UsableRulesProof
                ↳ PiDP
                  ↳ PiDPToQDPProof
                    ↳ QDP
                      ↳ Narrowing
                        ↳ QDP
                          ↳ UsableRulesProof
                            ↳ QDP
                              ↳ QReductionProof
                                ↳ QDP
                                  ↳ Instantiation
                                    ↳ QDP
                                      ↳ Instantiation
                                        ↳ QDP
                                          ↳ Instantiation
                                            ↳ QDP
                                              ↳ Instantiation
                                                ↳ QDP
                                                  ↳ Instantiation
                                                    ↳ QDP
                                                      ↳ Instantiation
                                                        ↳ QDP
                                                          ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

LOG2_IN(s(s(z0)), z1, z2) → LOG2_IN(s(s(s(z0))), z1, z2)
LOG2_IN(s(s(0)), s(z0), z1) → LOG2_IN(s(s(s(0))), s(z0), z1)
LOG2_IN(s(s(s(0))), s(z0), z1) → U31(s(0), s(z0), z1, small_out(0))
U31(s(0), s(z0), z1, small_out(0)) → LOG2_IN(s(0), s(s(z0)), z1)
U31(0, s(z0), z1, small_out(0)) → LOG2_IN(s(0), s(s(z0)), z1)
U31(s(z0), z1, z2, small_out(0)) → LOG2_IN(s(0), s(z1), z2)
LOG2_IN(s(0), s(z1), z2) → LOG2_IN(s(s(0)), s(z1), z2)
U31(z0, z1, z2, small_out(s(0))) → LOG2_IN(s(0), s(z1), z2)
LOG2_IN(s(s(0)), s(z0), z1) → U31(0, s(z0), z1, small_out(s(0)))
LOG2_IN(s(s(s(z0))), z1, z2) → U31(s(z0), z1, z2, small_out(0))
LOG2_IN(s(s(0)), s(z0), z1) → U31(0, s(z0), z1, small_out(0))
LOG2_IN(s(s(s(0))), s(z0), z1) → U31(s(0), s(z0), z1, small_out(s(0)))
LOG2_IN(s(s(s(z0))), z1, z2) → U31(s(z0), z1, z2, small_out(s(0)))

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule U31(z0, z1, z2, small_out(s(0))) → LOG2_IN(s(0), s(z1), z2) we obtained the following new rules:

U31(s(0), s(z0), z1, small_out(s(0))) → LOG2_IN(s(0), s(s(z0)), z1)
U31(s(z0), z1, z2, small_out(s(0))) → LOG2_IN(s(0), s(z1), z2)
U31(0, s(z0), z1, small_out(s(0))) → LOG2_IN(s(0), s(s(z0)), z1)



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ UsableRulesProof
                ↳ PiDP
                  ↳ PiDPToQDPProof
                    ↳ QDP
                      ↳ Narrowing
                        ↳ QDP
                          ↳ UsableRulesProof
                            ↳ QDP
                              ↳ QReductionProof
                                ↳ QDP
                                  ↳ Instantiation
                                    ↳ QDP
                                      ↳ Instantiation
                                        ↳ QDP
                                          ↳ Instantiation
                                            ↳ QDP
                                              ↳ Instantiation
                                                ↳ QDP
                                                  ↳ Instantiation
                                                    ↳ QDP
                                                      ↳ Instantiation
                                                        ↳ QDP
                                                          ↳ Instantiation
                                                            ↳ QDP
                                                              ↳ NonTerminationProof

Q DP problem:
The TRS P consists of the following rules:

LOG2_IN(s(s(z0)), z1, z2) → LOG2_IN(s(s(s(z0))), z1, z2)
LOG2_IN(s(s(0)), s(z0), z1) → LOG2_IN(s(s(s(0))), s(z0), z1)
LOG2_IN(s(s(s(0))), s(z0), z1) → U31(s(0), s(z0), z1, small_out(0))
U31(s(0), s(z0), z1, small_out(0)) → LOG2_IN(s(0), s(s(z0)), z1)
U31(0, s(z0), z1, small_out(0)) → LOG2_IN(s(0), s(s(z0)), z1)
U31(s(z0), z1, z2, small_out(0)) → LOG2_IN(s(0), s(z1), z2)
LOG2_IN(s(0), s(z1), z2) → LOG2_IN(s(s(0)), s(z1), z2)
LOG2_IN(s(s(0)), s(z0), z1) → U31(0, s(z0), z1, small_out(s(0)))
U31(s(0), s(z0), z1, small_out(s(0))) → LOG2_IN(s(0), s(s(z0)), z1)
LOG2_IN(s(s(s(z0))), z1, z2) → U31(s(z0), z1, z2, small_out(0))
LOG2_IN(s(s(0)), s(z0), z1) → U31(0, s(z0), z1, small_out(0))
U31(s(z0), z1, z2, small_out(s(0))) → LOG2_IN(s(0), s(z1), z2)
LOG2_IN(s(s(s(0))), s(z0), z1) → U31(s(0), s(z0), z1, small_out(s(0)))
U31(0, s(z0), z1, small_out(s(0))) → LOG2_IN(s(0), s(s(z0)), z1)
LOG2_IN(s(s(s(z0))), z1, z2) → U31(s(z0), z1, z2, small_out(s(0)))

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

The TRS P consists of the following rules:

LOG2_IN(s(s(z0)), z1, z2) → LOG2_IN(s(s(s(z0))), z1, z2)
LOG2_IN(s(s(0)), s(z0), z1) → LOG2_IN(s(s(s(0))), s(z0), z1)
LOG2_IN(s(s(s(0))), s(z0), z1) → U31(s(0), s(z0), z1, small_out(0))
U31(s(0), s(z0), z1, small_out(0)) → LOG2_IN(s(0), s(s(z0)), z1)
U31(0, s(z0), z1, small_out(0)) → LOG2_IN(s(0), s(s(z0)), z1)
U31(s(z0), z1, z2, small_out(0)) → LOG2_IN(s(0), s(z1), z2)
LOG2_IN(s(0), s(z1), z2) → LOG2_IN(s(s(0)), s(z1), z2)
LOG2_IN(s(s(0)), s(z0), z1) → U31(0, s(z0), z1, small_out(s(0)))
U31(s(0), s(z0), z1, small_out(s(0))) → LOG2_IN(s(0), s(s(z0)), z1)
LOG2_IN(s(s(s(z0))), z1, z2) → U31(s(z0), z1, z2, small_out(0))
LOG2_IN(s(s(0)), s(z0), z1) → U31(0, s(z0), z1, small_out(0))
U31(s(z0), z1, z2, small_out(s(0))) → LOG2_IN(s(0), s(z1), z2)
LOG2_IN(s(s(s(0))), s(z0), z1) → U31(s(0), s(z0), z1, small_out(s(0)))
U31(0, s(z0), z1, small_out(s(0))) → LOG2_IN(s(0), s(s(z0)), z1)
LOG2_IN(s(s(s(z0))), z1, z2) → U31(s(z0), z1, z2, small_out(s(0)))

The TRS R consists of the following rules:none


s = LOG2_IN(s(s(z0)), z1, z2) evaluates to t =LOG2_IN(s(s(s(z0))), z1, z2)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:



Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from LOG2_IN(s(s(z0)), z1, z2) to LOG2_IN(s(s(s(z0))), z1, z2).